Nuprl Definition : ma-send 11,40

M.send(k;l;s;v;ms;i)
== L != (M.2.2.2.2.2).1(<kl>)
== 
== ms = if source(l) = i then concat(map(tgf.map(x.<tgf.1, x>;(tgf.2)(s,v));L)) else [] fi  
latex



clarification:

M.send(k;l;s;v;ms;i)
== fpf-val(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);
== fpf-val(((M.2.2.2.2.2).1);
== fpf-val(<kl>;
== fpf-val(k,L.(ms
== fpf-val(k,L.(=
== fpf-val(k,L.(if source(l) = i
== fpf-val(k,L.(then concat(map(tgf.map(x.<tgf.1, x>;(tgf.2)(s,v));L))
== fpf-val(k,L.(else []
== fpf-val(k,L.(fi 
== fpf-val(k,L.( ((tg:Id  if source(l) = i then M.da(rcv(l,tg)) else Top fi ) List))) 
latex


Definitionsz != f(x P(a;z), product-deq(A;B;a;b), Knd, IdLnk, KindDeq, IdLnkDeq, s = t, type List, x:A  B(x), Id, M.da(a), rcv(l,tg), Top, if b then t else f fi , a = b, source(l), concat(ll), map(f;as), x.A(x), <ab>, t.1, f(a), t.2, []
FDL editor aliasesma-send

origin